The present invention pertains to verifying circuit designs. More particularly, the present invention pertains to an improved system for verification of VLSI (Very Large Scale Integration) designs.
Formal verification of the functioning of a digital design is a fundamental necessity with the increasing size and complexity as well as important functions to be executed by the digital design. Even more specifically, formal verification of a digital sequential system is needed, yet lacking, for those systems that are large and complex. The mathematical modeling techniques presently available for a digital sequential system, e.g., VHDL (Very High Speed Integrated Circuits (VHSIC) Hardware Description Language, e.g., standard VHDL-1076 (1987) as developed by Institute of Electrical and Electronic Engineers) and Verilog, are incapable of providing an efficient and confident verification review of some modem large and complex systems due in part to the complexity and memory requirements of the mathematical modeling technique.
A formal equivalence verification tool (FEV) is a CAD processing method used to ensure correct implementation of chip designs. Logic design size and complexity of chip designs are growing significantly in the field and present a challenge to the formal equivalence tool.
Formal equivalence verification, in the sequential domain particularly, is traditionally based on Binary Decision Diagrams (BDDs). Binary Decision Diagrams are graph structures that encode the state space or logic behavior and symbolic traversals of a Very Large Scale Integration (VLSI) logic design for all possible input value combinations. Unfortunately, because the huge state space of some modem Very Large Scale Integration (VLSI) designs, Binary Decision Diagrams cause memory complexity that cannot be confidently handled by the formal equivalence verification tool.
While most formal equivalence verification and state space traversal techniques remain infeasible for the required amount of memory of modem designs, common random binary simulation and Automatic Test Pattern Generator (ATPG) techniques also are not feasible because those techniques cover a relatively very small portion of the state space, thus providing poor or incorrect computed results. Further, some traditional techniques only perform a combinational equivalence check, thus not recognizing the equivalence of some sequentially equivalent circuits.
In xe2x80x9cSimulation-Based Sequential Equivalence Checking of RTL VHDLxe2x80x9d, by Fulvio Corno et al. for Politecnico di Torino, published in 1999 by IEEE (hereinafter referred to as xe2x80x9cCorno referencexe2x80x9d, the Corno reference""s algorithm appears based on genetic algorithms for producing meaningful test patterns for simulation, and interacts with a VHDL simulator. One shortcoming of the Corno reference is that it cannot provide any equivalence proof and is instead oriented towards finding a difference. The Corno reference discusses its prototype RAVE (RT-level Automatic Verificator) which proved in test runs to have low run times on moderately large circuits. RAVE, the RT-level Automatic Verificator, uses a genetic algorithm and when presented with two circuits to be proven equivalent, RAVE searches in the space of all possible input sequences for a counterexample, the counterexample being a sequence that generates a different output response in the two circuits. The Corno reference""s algorithms do not provide useful coverage for complex chip designs and instead the algorithms suffer from poor approximation due to low coverage of the space traversal.
In view of the above, there is a need for an efficient technique which can provide larger state space coverage and simultaneously produce high quality results.